T:Type, j:, l:(T List).
(0 < j)  (j  ||l||)  ((firstn(j - 1;l) @ [l[(j - 1)]]) ~ firstn(j;l)) 

latex

Definitions	x:A. B(x), P  Q, t  T, , A  B, A, False, i  j , SQType(T), {T}, as @ bs, firstn(n;as), l[i], hd(l), Y, if b then t else f fi , i <z j, nth_tl(n;as), tt, ff, i z j, b, Top, S  T, P  Q, P  Q, T, True, P & Q, tl(l), , Dec(P), P  Q, , Unit,
Lemmas	nat wf, le wf, length wf1, nat properties, ge wf, decidable int equal, list decomp, first0, tl wf, top wf, squash wf, true wf, length tl, lt int wf, bool wf, iff transitivity, assert wf, eqtt to assert, assert of lt int, le int wf, bnot wf, eqff to assert, bnot of lt int, assert of le int, bnot of le int